Inference at * 2 1 1 2 
Iof proof for Lemma fseg select:



1. T : Type
2. l1 : T List
3. l2 : T List
4. ||l1||  ||l2||
5. i:. (i < ||l1||)  (l1[i] = l2[((||l2|| - ||l1||)+i)])
6. l1 = nth_tl(||l2|| - ||l1||;l2)
  l2 = (firstn(||l2|| - ||l1||;l2) @ l1) 

latex

 by ((RW (AddrC [3;2] (HypC (-1))) 0) 
CollapseTHENA (Auto)) 

latex

C1: 

C1:   l2 = (firstn(||l2|| - ||l1||;l2) @ nth_tl(||l2|| - ||l1||;l2))
C.

Definitions	P  Q, P & Q, x:A  B(x), as @ bs, type List, x:A. B(x), , Type, T, s = t, P  Q, P  Q, x:AB(x), True, t  T
Lemmas	iff wf, rev implies wf, append wf, squash wf, true wf